zk-STARKs | FRI | MIMC

f(x)=yにおいて、めちゃ時間かかるfの計算の証明をめちゃ早い時間で検証できる。

zkの性質はVDFsへの応用を考える場合は必要なし。

MIMC

code: mimc.py

def mimc(inp, steps, round_constants):

start_time = time.time()

for i in range(steps-1):

print("MIMC computed in %.4f sec" % (time.time() - start_time))

return inp

MIMCは標数2の体上で演算するので加法演算はXOR。

MIMC自体もVDFsの性質を持っている。

つまり、VDFs的にはbackwardがcomuptingであり、forwardがverifying。

https://gyazo.com/d9529e3236af712a34d769c3cd7e40a6

STARKを用いることでMIMCを計算するよりも検証計算をより効率化することができる。

つまり、Proverがbackwardの計算を行い、forwardのSTARKを計算し、proofとして提供することでVerifierはそのSTARKを単に検証するだけでOK。

STARKの検証はオリジナルの計算量に限らず、python実装で~0.005-0.3sほど。

有限体の位数は 2^256 - 351 * 2^32 + 1

有限体上の多項式演算

Montgomery batch inversion

code: inv.py

# Modular inverse using the extended Euclidean algorithm

def inv(self, a):

if a == 0:

return 0

lm, hm = 1, 0

low, high = a % self.modulus, self.modulus

while low > 1:

r = high//low

nm, new = hm-lm*r, high-low*r

lm, low, hm, high = nm, new, lm, low

return lm % self.modulus

下図において、inputは紫、outputが緑、乗算が黒、そして赤のみがモジュラ逆数。

https://gyazo.com/b63c1fe9fc305dea69fb8f0ca19d8ead

code: multi_inv.py

def multi_inv(self, values):

for i in range(len(values)):

for i in range(len(values), 0, -1):

return outputs

多項式演算

QAP的に多項式は係数配列で扱う。

ある多項式をある特定のポイントで評価する演算。

code:eval_poly_at.py

# Evaluate a polynomial at a point

def eval_poly_at(self, p, x):

y = 0

power_of_x = 1

for i, p_coeff in enumerate(p):

y += power_of_x * p_coeff

power_of_x = (power_of_x * x) % self.modulus

return y % self.modulus

6x^2+5x+4を2で評価

高速フーリエ変換(FFTs, Fast Fourier Transforms)

ラグランジュの補間公式とdegree < N次多項式のNポイントを評価する計算はquadratic時間かかる。

例えば、1000ポイントのラグランジュ補間公式は数百万ステップが必要になる

なので、FFTで計算の効率化を図る。

FFTであれば、O(n*log(n))時間（例えば、1000ポイントであれば10,000ステップ）であるが、x座標はN=2^kに対する1の冪根である必要がある。つまり、p^N=1となるpがx座標でなければならない。

code:fft.py

def fft(vals, modulus, root_of_unity):

if len(vals) == 1:

return vals

for i, (x, y) in enumerate(zip(L, R)):

y_times_root = y*pow(root_of_unity, i, modulus)

return o

def inv_fft(vals, modulus, root_of_unity):

f = PrimeField(modulus)

# Inverse FFT

invlen = f.inv(len(vals))

return [(x*invlen) % modulus for x in

fft(vals, modulus, f.inv(root_of_unity))]

code:証明

>> f = poly_utils.PrimeField(337)

Montgomery batch inversionを用いたinverse FFTにより、

code:検証

となり、確かにinputと一致していることがわかる。（ここではzkを想定していないのでinputが分かってOK）

FRI (Fast Reed-Solomon Interactive Oracle Proofs of Proximity)

low-degree proofとは

要求した多項式が実際にその多項式であることがかなり少ないエラーで示されるマークルルート

input

（Verifierがクレームあるいはマークルルートのエントロピーにより選定された）低次元多項式を評価する値のセット

この値の数がdegreeより少ないことがlow-degree proof

1の冪根：多項式を評価するx座標

高速フーリエ変換を用いるため

modulus

code:column.py

# Calculate the set of x coordinates

xs = get_power_cycle(root_of_unity, modulus)

column = []

for i in range(len(xs)//4):

x_poly = f.lagrange_interp_4(

)

column.append(f.eval_poly_at(x_poly, special_x))

もしPがN次式であればP'(y) = Q(special_x, y)はN/4次式となる。

直接Q()を計算するのではなく、x^4の値に対してxと一致する4つの値があるのでQ(?, x**4)の値が4つあることになる

1, g, g^2, g^3

For any given value of x4, there are 4 corresponding values of x: x, modulus - x, and x multiplied by the two modular square roots of -1.

補間多項式をR(x)=Q(x, x**4)として、R(speacial_x)=Q(special_x, x**4)=P'(x**4)の計算

https://gyazo.com/cd3ac51b39a491ea7c9fc4bf86c62f8d

行（y座標）のmerkle rootをseedとして使ってx^4値のリストの中からランダムに40個くらいクエリし、proofとして利用する。

それぞれのクエリに対して、Q(?, x**4)の5つの値(その多項式からの4つの点と)のmerkle branchを提供する。

code:merkle_branch.py

m2 = merkelize(column)

# Pseudo-randomly select y indices to sample

# Compute the Merkle branches for the values in the polynomial and the column

branches = []

for y in ys:

検証タスクはこれの5つの値が同じ4次元多項式上に存在するか検証すること

STARK

tl;dr

各stepごとのtransition constraintsとinput, outputのboundary constraintsの検証をするためにそれぞれのconstraintsを多項式の問題にし、証明者が確かにその多項式を持っていることをかなり高い確率で証明する。

succinctにするために、low-degree proofで考える。つまり、次元数より少ない点のピックアップで確率的に多項式を復元できる方法。

具体的には、以前の状態から次の状態に正当に遷移していることを表す多項式C(P(x)) = 0 であることを示せればいいが、愚直にやるのはめちゃ計算コストがかかってしまう。なので、その代わりにZを最小多項式として CP= D * Z が全てのcomputational traceで成立することをFRI proofで確率的に示す。つまり、dataをかなり多くにextendして、少数のクエリを要求し、それらでCP=D*Zを示す。

検証者からのクエリに対して、merkle treeで証明者が多項式の存在証明を行うが、non-interactiveにするためにmerkle rootをseedに用い、そのmerkle rootが正しいことも問題に含める。

また、適切な位数の有限体演算、値に対して関数outputが一致する多項式の一括計算などにより証明・検証の効率性を高める。

MIMC関数のステップごとの中間値をcomputational traceとして生成。

code:generate_trace.py

# Generate the computational trace

for i in range(steps-1):

このcomputational traceをFFTで多項式に変換。

code:trace_fft.py

// g**steps = 1

computational_trace_polynomial = inv_fft(computational_trace, modulus, subroot)

// g2**(steps*8) = 1

p_evaluations = fft(computational_trace_polynomial, modulus, root_of_unity)

round constantsも多項式に変換可能。

8192ステップあり、64 round constantsだと仮定すると、g1^128の関数としてround constantsをFFTへ計算し、constants間はゼロにする。

stepが8192, round constantsが64だとすると、round constantsごとのstepは128なのでg1^128のroot of unityでFFTを計算する。

extension factor = 8の時、64 * 8 = 512 stepが繰り返されるので512stepだけを計算すれば良い。

https://gyazo.com/f45c5b98d83304bf7f317f8ec89083f2

g1: black

g2: purple

1: orange

しかし、全ての座標に対してQ(x) = 0が成り立つかどうか検証するのはオリジナルな計算よりも大きくなってしまうので、Q(x)がZ(x)の倍数であることを確率的に証明するアプローチ（FRI)をとる。

D(x) * Z(x) = Q(x)

Proverが扱うZ(x)はステップの数に応じて大きくなるが、verifyerは特定のxに対してのみ計算するのでsuccinct。

transition constraints - それぞれの連続的計算stepが正当か

boundary constraints - 計算のinputとoutputに対する検証 (snarksでいうwitness map?)

boundary constraints

P(1) = D(1), P(last_step) = D(last_step)を証明するだけでは他の残りのデータに対して同じ多項式上にあるか証明できない。

同様の多項式除算トリック

code:interpolant.py

# B = (P - I) / Z2

print('Computed B polynomial')

P(x) - I(x)が(1, input), (last_step, output)ではゼロになるので、(x-1)(x-last_step)の倍数であることを証明する。

P - I = B * Z2

CP = D * Zと一緒。

https://gyazo.com/73bedf743241628597f857e5a46663e9

P, D, B全てを証明する必要があるが、3つのFRI proofはexpensiveなので3つのランダムな線形和に対するFRI proofを行う。ランダムはP, D, Bのmerkle root。

code:linear_combination.py

# Compute the linear combination. We don't even bother calculating it

# in coefficient form; we just compute the evaluations

root_of_unity_to_the_steps = f.exp(root_of_unity, steps)

for i in range(1, precision):

for i in range(precision)]

m_rootがP,D,Bのmerkle root

l_evaluationsの線形和のランダム値に利用

l_rootがP,D,Bの次元チェックのためのランダム線形和のmerkle root

Dの次数が2*stepsよりも小さいか

PとBの次数がstepsよりも小さいか

stepsより大きいと愚直にやるよりも計算量が多くなってしまう

We want to prove that the degree of D is less than 2 * steps, and that of P and B are less than steps, so we actually make a random linear combination of P, P * xsteps, B, Bsteps and D, and check that the degree of this combination is less than 2 * steps.

全ての多項式に対するspot-check

code:spot_check.py

# Do some spot checks of the Merkle tree at pseudo-random coordinates, excluding

branches = []

samples = spot_check_security_factor

exclude_multiples_of=extension_factor)

for pos in positions:

branches.append(mk_branch(mtree, pos))

branches.append(mk_branch(mtree, (pos + skips) % precision))

branches.append(mk_branch(l_mtree, pos))

print('Computed %d spot checks' % samples)

proof

merkle roots

spot-checked branches

ランダム線形和のlow-degree proof

code:proof.py

branches,

prove_low_degree(l_evaluations, root_of_unity, steps * 2, modulus, exclude_multiples_of=extension_factor)]

verifierの検証

code:verify.py

for i, pos in enumerate(positions):

x = f.exp(G2, pos)

x_to_the_steps = f.exp(x, steps)

zvalue = f.div(f.exp(x, steps) - 1,

x - last_step_position)

k_of_x = f.eval_poly_at(constants_mini_polynomial, f.exp(x, skips2))

# Check transition constraints Q(x) = Z(x) * D(x)

assert (p_of_g1x - p_of_x ** 3 - k_of_x - zvalue * d_of_x) % modulus == 0

# Check boundary constraints B(x) * Z2(x) + I(x) = P(x)

assert (p_of_x - b_of_x * f.eval_poly_at(zeropoly2, x) -

f.eval_poly_at(interpolant, x)) % modulus == 0

# Check correctness of the linear combination

assert (l_of_x - d_of_x -

k1 * p_of_x - k2 * p_of_x * x_to_the_steps -

k3 * b_of_x - k4 * b_of_x * x_to_the_steps) % modulus == 0

C(P(x), P(g1*x), K(x)) = Z(x) * D(x)

最後のtrace以外に対して、次のtrace値がその前の値から計算して一致するか

transition constraintsに対する検証

B(x) * Z2(x) + I(x) = P(x)

boundary constraintsに対する検証

線形和の正当性

FRI proofの検証

constraintsをlow-degreeで検証できるようにするためのFRI proofの検証

STARKスキーム

それぞれのcomputtional traceで0になる最小多項式Z(x)を構築

D=CP / Z となる多項式Dを構築

PとDをmerkle treeに。

L = D + k * x ** steps * P 、kはP, Dのmerkle rootをベースに選定

上記のFRI proofを生成

Lのmerkle rootをseedにD*ZがCPと一致するかspot-check

おまけ

いくつのspot-checkをすればsoundnessは十分に満たされるのか

tutorialのpython実装のMIMCでは証明60sec, 検証0.2 secで300倍ほど

FFTを使うためにstepsとround constantsはk^2である必要がある

MiMC

evaluate the SNARK-friendly MiMChash function

Hash-based VDFs, MIMC and STARKs

STARKs資料まとめ

STARKよりもproof sizeが小さい。verify timeはスケールしていない。

code